(declare-fun _substvar_103_ () Bool)
(declare-fun _substvar_104_ () Bool)
(declare-fun _substvar_118_ () Bool)
(declare-fun _substvar_125_ () Bool)
(declare-fun _substvar_291_ () Bool)
(declare-fun _substvar_322_ () Bool)
(declare-fun _substvar_324_ () Bool)
(declare-fun uf3 (Bool Bool Bool) Bool)
(declare-const v7 Bool)
(declare-const i0 Int)
(declare-const v12 Bool)
(declare-const v14 Bool)
(assert (or v14 (distinct 4435 (div (- 25 i0 0 i0) 4435)) (< 0 (- 25 i0 0 i0))))
(assert (or (uf3 _substvar_103_ true (forall ((q0 Bool) (q1 Int) (q2 Int) (q3 Bool) (q4 Bool) (q5 Int)) (or (not (>= i0 q2)) _substvar_322_ _substvar_125_ v7 _substvar_118_))) _substvar_291_ v12))
(assert _substvar_104_)
(assert _substvar_324_)
(check-sat)
